Nuprl Lemma : length_sublist
11,40
postcript
pdf
T
:Type,
L1
,
L2
:(
T
List).
L1
L2
(||
L1
||
||
L2
||)
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
suptype(
S
;
T
)
,
S
T
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
L1
L2
,
{
i
..
j
}
,
Lemmas
sublist
wf
,
int
seg
wf
,
increasing
wf
,
non
neg
length
,
length
wf1
,
increasing
le
origin
T:Type, L1, L2:(T List). L1 
L2 
(||L1|| 
||L2||) T:Type, L1, L2:(T List). L1 L2 (||L1|| ||L2||) 
T Qx:A. B(x) T
x:A. B(x) L2
}